1. Field of the Invention
The present invention relates to finite state machines, and, in particular, to model checking of hierarchical state machines.
2. Description of the Related Art
Finite state machines (FSMs) are widely used in the modeling of systems in various areas. Descriptions using FSMs are useful to represent the flow of control (as opposed to data manipulation) and are amenable to formal analysis such as model checking. In the simplest setting, an FSM consists of a labeled graph whose vertices correspond to system states and whose edges correspond to system transitions.
In practice, to describe complex systems using FSMs, extensions from this basic FSM definition are useful, including the following three orthogonal extensions: (1) communicating FSMs, in which annotations are added so that transitions within different FSMs corresponding to different components can be synchronized; (2) extended FSMs, in which variables, such as counters and buffers, together with guarded assignments on transitions, are added to allow succinct description; and (3) hierarchical or nested FSMs, in which vertices of an FSM can be ordinary states or superstates that are themselves FSMs. While the impact of adding the first two features to the complexity of analysis problems has been well understood, this has not been the case with regard to the impact of the third feature.
The ability to nest FSMs is common in many specification formalisms and methods. It is a central component of various object-oriented software development methodologies that have been developed in recent years. This capability is commonly available also in commercial computer-aided software engineering tools that are coming out.
The nesting capability is useful also in formalisms and tools for the requirements and testing phases of the software development cycle. On the requirements side, it is used to specify scenarios (or use cases) in a structured manner. For instance, the International Telecommunication Union (ITU) standard Z.120 for message sequence charts formalizes scenarios of distributed systems in terms of hierarchical graphs built from basic message sequence charts. On the testing side, FSMs are used often to model systems for the purpose of test generation, and again the nesting capability is useful to model large systems. This is useful for systems with informal and incomplete requirements and design documentation, as is often the case, and especially for software that was developed and evolved over a long period of time, when the test models are updated for continued regression testing as the system evolves.
An example of a hierarchical FSM is a digital clock. The top-level state machine for a digital clock may consist of a cycle through 24 superstates, with each superstate corresponding to a different hour of the day. Each such state, in turn, is a hierarchical state machine consisting of a cycle through 60 superstates counting minutes, each of which, in turn, is an (ordinary) state machine consisting of a cycle counting 60 seconds.
Hierarchical state machines have two descriptive advantages over ordinary FSMs. First, superstates offer a convenient structuring mechanism that allows a system to be specified in a stepwise refinement manner, where the system can be viewed at different levels of granularity. Such structuring is particularly useful for specifying large FSMs via a graphical interface. Second, by allowing sharing of component FSMs, components need to be specified only once and then reused in different contexts, leading to modularity and succinct system representations. For instance, the 24 superstates of the top-level FSM for the digital clock can be mapped to the same hierarchical FSM corresponding to an hour, and the 60 superstates corresponding to the minutes of each hour can be mapped to the same ordinary FSM corresponding to a second.
Model checking is emerging as a practical tool for detecting logical errors in early stages of system design. As such, model checking is particularly useful in automated debugging of complex reactive systems such as embedded controllers and network protocols. In model checking, a high-level description of a system is compared against a correctness requirement to discover inconsistences.
The straightforward approach to applying model checking to a hierarchical state machine is to flatten it (i.e., recursively substitute each superstate with its associated FSM) and then apply a model checking tool to the resulting ordinary FSM. Such flattening, however, can cause a large blow-up in the size of the state machine, particularly when there is a lot of sharing of component FSMs. For instance, the hierarchical description of the digital clock has 24+60+60=144 vertices, while the equivalent flattened FSM has 24*60*60=86,400 vertices. Thus, if the hierarchical state machine is first flattened and then subjected to a conventional model checking algorithm, the worst-case complexity would be exponential in the original description of the structure. The amount of computer memory needed to represent such flattened FSMs can be prohibitively large.